/*
 * SYmbolic Model-Based test case generation toOL for Real-Time systems (SYMBOLRT)
 * (C) Copyright 2010-2012 Federal University of Campina Grande (UFCG)
 * 
 * This file is part of SYMBOLRT.
 *
 * SYMBOLRT is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 *
 * SYMBOLRT is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with SYMBOLRT.  If not, see <http://www.gnu.org/licenses/>.
 *
 *
 * REVISION HISTORY:
 * Author                           Date           Brief Description
 * -------------------------------- -------------- ------------------------------
 * Wilkerson de Lucena Andrade      19/04/2012     Initial version
 * 
 */
package br.edu.ufcg.symbolrt.main;

import java.util.List;

import br.edu.ufcg.symbolrt.algorithms.CompositionCompletion;
import br.edu.ufcg.symbolrt.algorithms.ParallelComposition;
import br.edu.ufcg.symbolrt.algorithms.SequentialComposition;
import br.edu.ufcg.symbolrt.algorithms.SequentialCompositionShared;
import br.edu.ufcg.symbolrt.algorithms.SynchronousProduct;
import br.edu.ufcg.symbolrt.algorithms.TestPurposeCompletion;
import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.Transition;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.compiler.facade.Compiler;
import br.edu.ufcg.symbolrt.examples.Mouse;
import br.edu.ufcg.symbolrt.examples.Screen;
import br.edu.ufcg.symbolrt.examples.ScreenImp;
import br.edu.ufcg.symbolrt.examples.TargetDesignation;
import br.edu.ufcg.symbolrt.examples.TargetTracking;
import br.edu.ufcg.symbolrt.examples.Toy5;
import br.edu.ufcg.symbolrt.examples.Toy6;
import br.edu.ufcg.symbolrt.exception.ClockGuardException;
import br.edu.ufcg.symbolrt.exception.IncompatibleOperationException;
import br.edu.ufcg.symbolrt.facade.SYMBOLRT;
import br.edu.ufcg.symbolrt.symbolicexecution.algorithms.SymbolicExecution;
import br.edu.ufcg.symbolrt.symbolicexecution.algorithms.TestCaseSelection;
import br.edu.ufcg.symbolrt.symbolicexecution.algorithms.TestTreeTransformation;
import br.edu.ufcg.symbolrt.symbolicexecution.base.SymbolicExecutionTree;
import br.edu.ufcg.symbolrt.symbolicexecution.base.SymbolicState;
import br.edu.ufcg.symbolrt.symbolicexecution.base.SymbolicTransition;
import br.edu.ufcg.symbolrt.symbolicexecution.exception.SymbolicValueNameException;
import br.edu.ufcg.symbolrt.util.Constants;
import br.edu.ufcg.symbolrt.util.GraphVisualization;


/**
 * <code>Main</code> Class. <br>
 * This class contains the main for executing the SYMBOLRT tool.
 * 
 * @author Wilkerson de Lucena Andrade  ( <a href="mailto:wilkerson@computacao.ufcg.edu.br">wilkerson@computacao.ufcg.edu.br</a> )
 * 
 * @version 1.0
 * <br>
 * SYmbolic Model-Based test case generation toOL for Real-Time systems (SYMBOLRT)
 * <br>
 * (C) Copyright 2010-2012 Federal University of Campina Grande (UFCG)
 * <br>
 * <a href="https://sites.google.com/a/computacao.ufcg.edu.br/symbolrt">https://sites.google.com/a/computacao.ufcg.edu.br/symbolrt</a>
 */
public class MainMouseScreenInputComplete {	
	
    public static void main(String[] args) {
    	
        GraphVisualization tiostsVis = new GraphVisualization();
        
        TIOSTS spec = generateCompletionScreen();
        //TIOSTS spec = generateCompletionMouse();
        tiostsVis.save(spec);
        
        TIOSTS tp = createTestPurpose();
        tiostsVis.save(tp);
        
        TestPurposeCompletion completionOperation = TestPurposeCompletion.getInstance();
        TIOSTS tpComplete = null;
        try {
                tpComplete = completionOperation.complete(tp);
        } catch (ClockGuardException e) {
                System.out.println(e.getMessage());
        }
        tiostsVis.save(tpComplete);
        
        SynchronousProduct synchronousOperation = SynchronousProduct.getInstance();
        TIOSTS sp = null;
        try {
                sp = synchronousOperation.synchronousProduct(spec, tpComplete);
        } catch (IncompatibleOperationException e) {
                System.out.println(e.getMessage());
        }
        tiostsVis.save(sp);
        
        // *********************** Symbolic Execution *********************** 
        SymbolicExecution symb = SymbolicExecution.getInstance();
        SymbolicExecutionTree zset = null;
        try {
                zset = symb.execute(sp);
        } catch (SymbolicValueNameException e) {
                System.out.println(e.getMessage());
        }
        
        // *********************** Test Case Selection ***********************
        TestCaseSelection tc = TestCaseSelection.getInstance();
        List<SymbolicExecutionTree> testCases = tc.selectAllTestCases(zset);
        
        System.out.println("Number of TCs: " + testCases.size());
        printZSET(testCases.get(0));
        
        
        // *********************** Test Tree Transformation ***********************
        TestTreeTransformation tt = TestTreeTransformation.getInstance();
        TIOSTS testCase = tt.translateTestTree(testCases.get(0), sp);
        
        tiostsVis.save(testCase);
}
    
    public static TIOSTS generateCompletionScreen(){
		//Inputs for parallel composition
		TIOSTS tiosts2 = Screen.createSPEC();
		//Building an implementation screen model not conformant to its specification
		CompositionCompletion compCompletion = CompositionCompletion.getInstance();
		TIOSTS resultScreen = null;		
					
		try {	
			resultScreen = compCompletion.complete(tiosts2);

		} catch (IncompatibleOperationException e) {
			e.printStackTrace();
		}catch (ClockGuardException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
		
		return resultScreen;    	
    }
    
    public static TIOSTS generateCompletionMouse(){
		//Inputs for parallel composition
		TIOSTS tiosts1 = Mouse.createSPEC();
		//Building an implementation screen model not conformant to its specification
		CompositionCompletion compCompletion = CompositionCompletion.getInstance();
		TIOSTS resultScreen = null;		
					
		try {	
			//resultMouse = compCompletion.complete(tiosts1);
			resultScreen = compCompletion.complete(tiosts1);

		} catch (IncompatibleOperationException e) {
			e.printStackTrace();
		}catch (ClockGuardException e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
		
		return resultScreen;    	
    }
	
    public static void printZSET(SymbolicExecutionTree zset) {
        System.out.println("*********************** States ***********************");
        for (SymbolicState zses : zset.getSymbolicStates()) {
                System.out.println(zses.toString() + "\n\n");
        }
        
        System.out.println("*********************** Transitions ***********************");
        for (SymbolicState zses : zset.getSymbolicStates()) {
                for (SymbolicTransition t : zses.getChildrenTransitions()) {
                        System.out.println(t.toString() + "\n");
                }
        }
}
	
    public static TIOSTS createTestPurpose(){
        TIOSTS tiosts = new TIOSTS("TP");
        
        //Parametros
        TypedData position = new TypedData("position", Constants.TYPE_INTEGER);
        tiosts.addActionParameter(position);

        // Input, output, and internal actions
        //Action init = new Action("initS", Constants.ACTION_INTERNAL);
        Action init = new Action("initS", Constants.ACTION_INTERNAL);
        tiosts.addAction(init);
        //Action simpleClick = new Action("simpleClick", Constants.ACTION_OUTPUT);
        Action simpleClick = new Action("simpleClick", Constants.ACTION_INPUT);
        simpleClick.addParameter(position.getName());
        tiosts.addAction(simpleClick);
        
        // Locations
        Location start = new Location("START");
        tiosts.addLocation(start);
        Location accept = new Location(Constants.VERDICT_ACCEPT);
        tiosts.addLocation(accept); 
        Location s6 = new Location("S6");
        tiosts.addLocation(s6);
        
        // Initial Condition
        tiosts.setInitialCondition(Constants.GUARD_TRUE);
        
        // Initial Location
        tiosts.setInitialLocation(start);

        // Transitions
        tiosts.createTransition("START", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init, null, null, "S6");
        tiosts.createTransition("S6", Constants.GUARD_TRUE, Constants.GUARD_TRUE, simpleClick, null, null, Constants.VERDICT_ACCEPT);
        
        return tiosts;
}
    
}
